COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	.require "let.pub" source file
C00009 ENDMK
C⊗;
.require "let.pub" source file;
.FONT c "SUB";
∂AIL Dr. Masahiko Sato↓Research Institute for Mathematical Sciences
↓Kyoto University↓Kyoto Japan∞

Dear Dr. Sato:

	I got an ARPAnet message from Reddy's secretary saying that
they had received a letter from Hayashi inquiring about our paper
and saying that they had accepted it as a short communication and
sent the special paper.  They wondered if I had been notified instead
of Hayashi, but I had received nothing about it.  No doubt they are
communicating with you.

	I now think I understand how to do non-knowledge and why we
were having trouble formalizing it.  My current view is that it
requires sentence schemata rather than sentences to express it.
Here is a schema expressing what can be derived
from the proposition %2Sees(Wise1,p1,p2)%1 that the first wise man
knows the colors of the spots of the others and that all he knows
can be derived from that.

.begin
.skip 1
.turn on "∂"
.nofill
(1)∂8%Btrue Sees(Wise1,p2,p3) ⊃ 
∂(20)[(true p2 ⊃ FF(p2)) ∧ (¬true p2 ⊃ FF(not p2))
∂(20)(true p3 ⊃ FF(p3)) ∧ (¬true p3 ⊃ FF(not p3))
∂(20)∧ ∀p.(axiom p ⊃ FF(p))
∂(20)∧ ∀pq.(FF(p) ∧ FF(p implies q) ⊃ FF(q))
∂(23)⊃ ∀p.(Knows(Wise1,p) ⊃ FF(p))]%1.
.end

	The formalism I am using here is essentially my syntactic formalism
as used in our paper but translated into predicate calculus in the
following way:

	1. The variables %2p%1, etc. represent propositions and
are asserted by writing %2true p%1.  Propositions are combined by
connectives %2and, or%1 and %2not%1 and the function %2Knows%1.

	2. We have axioms like

	%B∀w p.(true Knows(w,p) ⊃ true p)%1,

	%B∀w p.(true Knows(Fool,Knows(w,p) implies p))%1,

and

	%B∀p q.(true(p and q) ≡ true p ∧ true q)%1.

I have not taken the time to write my other axioms in this notation.

.xgenlines←xgenlines-2;
	3. %2Sees(Wise1,p1,p2)%1 should be a proposition that
can be known.  In order to make this possible, we will have to get rid of
the internal quantifiers in (1).

	In (1) above, %2FF%1 is a predicate parameter with implicit
universal quantification.  In order to apply the schema to show that
%B¬true Knows(Wise1,p1)%1, we must find a predicate to substitute for
%BFF%1 such that %B¬FF(p1)%1 and which satisfies (1), i.e. assigns
satisfies %2FF(p2)%1 and %2FF(p3)%1 since %2Wise1%1 knows these facts
and is preserved under reasoning.

	I think we can find such predicates, but I have not succeeded
so far, and I want to consult you and your colleagues about the
following specific point in addition to hoping for your collaboration
in general:

	In one sense finding such a predicate should be trivial; it
assigns false to %2FF(p1)%1 and true to %2FF(p2)%1 and %2FF(p3)%1,
and %2essentially%1 that's all we should have to say.  The complication
is that the language contains all sorts of additional assertions about
who knows what.  However, it seems intuitively clear that since
nothing is asserted about what %2Wise1%1 knows beyond the axioms,
a predicate which makes an arbitrary assignment
to the %2p%ci%1's must be extendable to one which is preserved
under reasoning.  In fact, it seems to me that there must be
something to this effect in your thesis where you show that
the theory is decideable.  In a sense, this is a strong form
of consistency - we need not only that the theory has models
but that certain partial interpretations are extendable to
models.

	There may be other kinds of other knowledge that %2Wise1%1 could
have that wouldn't give him any more knowledge of the physical
world.
For example, he could know that %2Wise2%1 knows whether he knows %2p1%1.

	Using these such schemata is like doing mathematical induction,
and we might even call their use %2knowledge induction%1.  My present
intuition is that schemata or something equivalent to them are
essential unless we build an axiomatization of knowledge that is
like Goedel-Bernays set theory in containing machinery for
building up the equivalent of classes.

.reg

P.S. I enclose a draft which discusses some of these matters, but
I have somewhat changed my point of view since it was written.  In
particular there are many ways of writing the schemata, so I wouldn't
emphasize so much the precise form of %2minimal inference%1 given
in that draft.